COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb A DIFFICULT VERIFICATION PROBLEM


	Consider a graph defined by a function %2successors%1.
We are interested in defining and proving correct a LISP function
for computing the component %2component x%1 of
a vertex %2x%1.  The component can be defined by the formula

	%2∀ x y:[y ε component x ≡ ∃ u:
x = qa u ∧ y = last u ∧ ∀ z1 z2:[precedes[z1,z2,u]
⊃ z2 ε successors z1]]%1,

where %2precedes[z1,z2,u]%1 is recursively defined by

	%2precedes[z1,z2,u] = ¬qn u ∧ [[z1 = qa u ∧ ¬qn qd u
∧ z2 = qad u] ∨ precedes[z1,z2,qd u]]%1.

	Our object is to define a LISP function computing
%2component x%1 and to prove that it is in accordance
with the above predicate calculus definition.  In order that
this should be possible we need an axiom stating that the
function %2successors%1 leads only to a finite graph.
This can be done in several ways, and one of the simplest
is to assert the existence of an integer %2N%1 that is
an upper bound on the length of a successor chain.

	A candidate function is

	%2component[x] = comp1[<x>,qnil]%1,

where

	%2comp[u,seen] = qif qn u qthen seen
qelse qif qa u ε seen qthen comp[qd u,seen]
qelse comp[successors[qa u]*[qd u],[qa u].seen]%1.

The inductions required to prove that this or any other solution
satisfies the specifications promise to be interesting.